<html>
<head><meta charset="utf-8"><title>relations-between-regions · t-compiler/wg-nll · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/index.html">t-compiler/wg-nll</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html">relations-between-regions</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="128284014"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128284014" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128284014">(Jun 19 2018 at 03:28)</a>:</h4>
<p>Hello! I hope this is the right place to ask a question about the "alias-based formulation of the borrow checker" blog post [0]? Specifically, I had a question about the "Relations between regions" section in the blog post.</p>
<p>For example, on line <code>let r: &amp;'1 mut Vec&lt;&amp;'2 i32&gt; = &amp;'3 mut v</code>it is asserted that both '0: '2 and '2: '0 hold. I would have expected the former ('0: 2) to hold, but not necessarily the latter ('2: '0). What happens if another vector is assigned to reference <code>r</code>?</p>
<p>I would greatly appreciate if someone could clarify how these "region" subset facts are computed in general. If possible, I would like to follow the example in detail to the end (e.g., a later argument relies on '4: '5: '2: '0).</p>
<p>Many thanks in advance!</p>
<p>[0] <a href="http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/" target="_blank" title="http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/">http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/</a></p>



<a name="128292737"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128292737" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128292737">(Jun 19 2018 at 08:14)</a>:</h4>
<p>they derive from the subtyping relationships and other parts of the MIR type check; in that particular case, <code>&amp;mut T</code> is invariant with respect to <code>T</code>, so <code>&amp;mut T &lt;: &amp;mut U</code> requires that <code>T = U</code> (and hence that <code>&amp;'2 i32 = &amp;'0 i32</code> in this particular example). <code>'2 = '0</code> if <code>'2: '0</code> and <code>'0: '2</code></p>



<a name="128321728"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128321728" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128321728">(Jun 19 2018 at 18:55)</a>:</h4>
<p>Thanks! From an alias analysis perspective, using similar reasoning as above, I find it surprising that <code>'0 = '1 = '3</code> would hold (rather than merely <code>'0 : '3</code> and <code>'1: '3</code>) in the following example where <code>u : Vec&lt;&amp;'0 i32&gt;</code> and <code>v : Vec&lt;&amp;'1 i32&gt;</code> are two different vectors:</p>
<p><code>a. let mut r: &amp;'2 mut Vec&lt;'3 &amp;i32&gt;;
 b. r = &amp;'4 mut v;
 c. r = &amp;'5 mut u;</code> </p>
<p>Is there any documentation that I could read to better this case? My confusion may stem from the fact that I think too much about alias analysis rather than type checking. In particular, I am reading subsets such as <code>'4 : '2</code> and <code>'5 : '2</code> to be similar to the subsets in Andersen's algorithm.</p>



<a name="128322296"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128322296" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128322296">(Jun 19 2018 at 19:06)</a>:</h4>
<p>I don't believe I said that <code>'1 </code> and <code>'3</code> would be related</p>



<a name="128322310"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128322310" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128322310">(Jun 19 2018 at 19:07)</a>:</h4>
<p>I'm not sure if we're talking about precisely the same example :)</p>



<a name="128329336"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128329336" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128329336">(Jun 19 2018 at 21:28)</a>:</h4>
<p>Sorry, I sought to illustrate the second part of my earlier question, namely: "What happens if another vector is assigned to reference r?"</p>
<p>On the surface, both examples share in common that they require a region <code>'R</code> as in <code>Vec&lt;'R &amp;i32&gt;</code> to be related to another region:</p>
<p>1\ Specifically, in the first example, reference <code>r</code> is only assigned once (using <code>v</code>) and <code>'R</code> turns out to be equal to another region.<br>
2\ In the second example, <code>r</code> is assigned twice (using <code>u</code> and <code>v</code>), but your response indicates that no such region _equality_ is induced then.</p>
<p>My goal was to better understand by comparing and contrasting both examples. Any suggestion that may get me back on the right track are welcome! :)</p>



<a name="128329638"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128329638" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128329638">(Jun 19 2018 at 21:33)</a>:</h4>
<blockquote>
<p>Any suggestion that may get me back on the right track are welcome! :)</p>
</blockquote>
<p>In other words, eventually if possible, I would like to be able to pick apart both examples by appealing to the right inference rules that are being used to setup the subset region relationships. I know a bit weird maybe, I am just curious.</p>



<a name="128364548"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128364548" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128364548">(Jun 20 2018 at 14:13)</a>:</h4>
<p><span class="user-mention" data-user-id="119443">@Alex Horn</span> An important point in Polonius is that the relations are per program point. So, in your second example, you will get that the relation <code>'3 = '1</code> holds on a set of program points, and the relation <code>'3 = '0</code> holds on some other set of points. Only if these two sets overlap, you will get a relation <code>'1 = '0</code>.</p>



<a name="128364550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128364550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128364550">(Jun 20 2018 at 14:13)</a>:</h4>
<p>Does this help?</p>



<a name="128370738"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128370738" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128370738">(Jun 20 2018 at 16:28)</a>:</h4>
<p>This helps, thank you! What I am still unclear about is: when do sets of program points "overlap"? I understood the <code>cfg_edge(P, Q)</code> fact and has it is used to propagate subset relations. In the second example, <code>cfg_edge(a, b)</code> and <code>cfg_edge(b, c)</code>.</p>



<a name="128374075"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128374075" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128374075">(Jun 20 2018 at 17:47)</a>:</h4>
<p>Niko in his blog post does not talk about at which program points a specific relation holds. Instead, he talks about what relations hold at a specific program point, which is basically the same thing just phrased differently. For example, the fact <code>subset(R1, R2, P)</code> expresses that the subset relation between regions <code>R1</code> and <code>R2</code> holds at the program point <code>P</code>. Now if you have a set of <code>subset</code> facts, you can compute at which set of program points <code>P</code> the subset relation between <code>R1</code> and <code>R2</code> holds.</p>



<a name="128374221"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128374221" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128374221">(Jun 20 2018 at 17:50)</a>:</h4>
<p>To answer your question: a set of program points that expresses the subset relation between <code>R1</code> and <code>R2</code> overlap with a set of program points that expresses the relation between <code>R2</code> and <code>R3</code> if there exists such a program point <code>P</code> that the facts <code>subset(R1, R2, P)</code> and <code>subset(R2, R3, P)</code> can be derived.</p>



<a name="128374253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128374253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128374253">(Jun 20 2018 at 17:51)</a>:</h4>
<p>Is it clearer?</p>



<a name="128382758"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128382758" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128382758">(Jun 20 2018 at 20:50)</a>:</h4>
<p>Awesome, thanks for taking the time to clarify; I appreciate it!</p>
<p>Let me make sure I understand. Here is a proof of <code>'0 = '1 = '3</code> for the second example:</p>
<p>As previously discussed, we know that the relation <code>'3 = '0</code> holds at program point <code>b</code>. Similarly,  <code>'3 = '1</code> at program point <code>c</code>. By definition, <code>cfg_edge(b, c)</code>. Hence, by <code>Rule subset3 (version 1)</code>, <code>'3 = '0</code> at program point <code>c</code>. Therefore, since <code>'3 = '0</code>and <code>'3 = '1</code> at  program point <code>c</code>, we conclude <code>'0 = '1 = '3</code>.</p>
<p>I find this equality surprising. Is this result expected?</p>
<p>One of <span class="user-mention" data-user-id="116009">@nikomatsakis</span> 's earlier comments reads: "I don't believe I said that <code>'1</code>  and <code>'3</code> would be related". I did not fully understand his comment. May I am misinterpreting the later assertion that we "will get that the relation <code>'3 = '1</code>" .</p>



<a name="128383816"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128383816" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128383816">(Jun 20 2018 at 21:12)</a>:</h4>
<p>sorry <span class="user-mention" data-user-id="119443">@Alex Horn</span>, I'm multi-plexing a bunch of stuff lately, but I'm finding it hard to understand your examples. =) Probably if I went back up and re-read your examples I would understand better. I would however appreciate copying and pasting all the information together in one place (i.e., not referencing any previous message :) Just looking at what I see in zulip I still don't quite see where <code>'0 = '1 = '3</code> is coming from etc. (For example, I don't know what program point c or b refers to, etc.)</p>
<p>I would like to see the input program (ideally in MIR-like format, but Rust-like is ok too).</p>



<a name="128400582"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128400582" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128400582">(Jun 21 2018 at 05:19)</a>:</h4>
<p>Will definitely do, I shall draft something. Thanks.</p>



<a name="128429779"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128429779" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128429779">(Jun 21 2018 at 17:44)</a>:</h4>
<p>I've created a v0-draft: <a href="https://pastebin.com/w53KTyzs" target="_blank" title="https://pastebin.com/w53KTyzs">https://pastebin.com/w53KTyzs</a>.</p>
<p>To keep things simple, the live analysis is assumed to be disabled.</p>
<p>What are the intended relations between the regions here?</p>
<p>If <code>'0 == '1 == '7</code> holds (which may or may not be the case), what are the implications on the analysis (if any)?</p>
<p>To further guide the discussion, I repeat (at times verbatim) what I understood our discussion to imply about the v0-example:</p>
<p>A\ On line 15 (<code>r = &amp;/* '8 */ mut u</code>), <code>&amp;mut T</code> is invariant with respect to<code>T</code>, so <code>&amp;mut T &lt;: &amp;mut U</code> requires that <code>T = U</code>. Hence, <code>'0 = '7</code>.<br>
B\ Similarly on line 18 (<code>r = &amp;/* '9 */ mut v</code>), <code>'1 = '7</code>.<br>
C\ By definition, <code>cfg_edge(line 17,  line 18)</code>(transitively).<br>
D\ Hence, by <code>Rule subset3 (version 1)</code>, we get <code>'0 = '7</code> on line 18.<br>
E\ Therefore, since <code>'0 = '7</code> and <code>'1 = '7</code> on line 18, <code>'0 = '1 = '7</code> holds.</p>



<a name="128436845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128436845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128436845">(Jun 21 2018 at 20:05)</a>:</h4>
<p>I think we're all confused about this <code>'0 = '1</code> notation, what is this all about?</p>



<a name="128436853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128436853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128436853">(Jun 21 2018 at 20:05)</a>:</h4>
<p>do you mean <code>'0: '1</code> instead?</p>



<a name="128438654"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128438654" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128438654">(Jun 21 2018 at 20:42)</a>:</h4>
<p><code>'0 = '1</code> I believe means <code>'0: '1</code> and <code>'1: '0</code></p>



<a name="128438679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128438679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128438679">(Jun 21 2018 at 20:42)</a>:</h4>
<p><span class="user-mention" data-user-id="119443">@Alex Horn</span> I looked at the example and <a href="https://gist.github.com/nikomatsakis/0eb5ba344e939b678fcad5452c82366c" target="_blank" title="https://gist.github.com/nikomatsakis/0eb5ba344e939b678fcad5452c82366c">wrote some notes</a></p>



<a name="128438701"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128438701" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128438701">(Jun 21 2018 at 20:43)</a>:</h4>
<p>One part of it is the liveness results — those currently cause the two assignments to <code>r</code> to be distinguished</p>



<a name="128438709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128438709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128438709">(Jun 21 2018 at 20:43)</a>:</h4>
<p>I think that is an element of the system we might change; but if we did so, then it would yes imply a loss of resolution</p>



<a name="128438747"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128438747" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128438747">(Jun 21 2018 at 20:44)</a>:</h4>
<p>is that what you are saying?</p>



<a name="128441245"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128441245" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Horn <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128441245">(Jun 21 2018 at 21:35)</a>:</h4>
<p>Read your notes, very enlightening. Yes, I am aiming to better understand the strengths and weaknesses of the proposed approach, which I find very interesting. In addition, I am curious how it relates to previous work, in case they are lessons from the past that could broaden my perspective.</p>



<a name="128466107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/relations-between-regions/near/128466107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/relations-between-regions.html#128466107">(Jun 22 2018 at 10:27)</a>:</h4>
<p>I'd appreciate any insights :)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>